Nuprl Lemma : es-locl-trans
11,40
postcript
pdf
the_es
:event_system{i:l}. trans(es-E(
the_es
);
x
,
y
.es-locl(
the_es
;
x
;
y
))
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
P
Q
Lemmas
es-axioms
,
event
system
wf
origin
the_es:event_system{i:l}. trans(es-E(the_es); x,y.es-locl(the_es; x; y)) the_es:event_system{i:l}. trans(es-E(the_es); x,y.es-locl(the_es; x; y)) x:A. B(x)
T
Q